T:Type, L:(T List), a,b:T. l_before(a; b; L; T)  (b  L) 

latex

Definitions	t  T, l_before(x; y; l; T), P  Q, x:A. B(x), if b then t else f fi , ff, tl(l), null(as), b, A, P  Q, P  Q, P  Q, False, prop{i:l}
Lemmas	sublist wf, member iff sublist, sublist transitivity, false wf, sublist tl, sublist weakening